$\forall$$T$, ${\it T'}$:Type$_{\mbox{\scriptsize i}}$, $L$:$T$ List, $f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$${\it T'}$), $P$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$$x$, $y$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ $P$($f$($x$),$f$($y$))) $\Rightarrow$ ($\forall$$x$,$y$$\in$mapl($f$;$L$).$P$($x$,$y$))